package minsat;

import java.io.FileNotFoundException;
import java.io.PrintWriter;
import java.io.UnsupportedEncodingException;
import java.util.List;
import java.util.Map;
import java.util.Random;

/**
 * This file contains some simple tests and tools used during development and is not intended for serious
 * evaluation, but is provided in the event that its contents are useful or illuminating to the
 * evaluator.
 * 
 * Tools include a random formula generator and a method that invokes this generator on both the
 * optimal and MinSatz algorithms repeatedly, writing the results to a file.
 */
public class Testing
{
  public static void main(String[] args)
  {
    try {
      compareSolveRandom(100);
    }
    catch (FileNotFoundException e) {
      e.printStackTrace();
    }
    catch (UnsupportedEncodingException e) {
      e.printStackTrace();
    }
  }

  /**
   * Solves a specified number of random MinSat instances using both the MinSatz solver and the
   * optimal solver for comparison. Results are written to a CSV.
   */
  private static void compareSolveRandom(int instances) throws FileNotFoundException,
      UnsupportedEncodingException
  {
    PrintWriter write = new PrintWriter("minsatz.csv", "UTF-8");
    Formula f;
    long startTimeMinSatz, stopTimeMinSatz, startTimeOptimal, stopTimeOptimal;
    double minSatzScore, optimalScore;
    Map<String, Boolean> minSatzMap, optimalMap;
    write.println("run;formula;minSatzMap;minSatzScore;minSatzTime;optMap;optScore;optTime");
    for (int x = 0; x < instances; x++) {
      f = generateRandomFormula(3, 25, 25, 20);
      startTimeMinSatz = System.currentTimeMillis();
      BindingsAndBound minSatzResult = MinSatz.runMinSatz(f, new BindingsAndBound(), null);
      stopTimeMinSatz = System.currentTimeMillis();
      System.out.println("MinSatz " + x + " completed in " + (stopTimeMinSatz - startTimeMinSatz));
      minSatzMap = MinSatz.convertToMap(minSatzResult);
      minSatzScore = f.evaluate(minSatzMap);
      startTimeOptimal = System.currentTimeMillis();
      optimalMap = MinSatz.optimalSat(f);
      stopTimeOptimal = System.currentTimeMillis();
      System.out.println("Optimal " + x + " completed in " + (stopTimeOptimal - startTimeOptimal));
      optimalScore = f.evaluate(optimalMap);
      write.println(x + ";" + f + ";" + minSatzMap + ";" + minSatzScore + ";"
          + (stopTimeMinSatz - startTimeMinSatz) + ";" + optimalMap + ";" + optimalScore + ";"
          + (stopTimeOptimal - startTimeOptimal));
    }
    write.close();
  }

  /**
   * Generates a random MinSat instance.
   * 
   * @param litPerClause Number of literals in every clause
   * @param totalLit Total number of unique literals
   * @param totalClause Total number of clauses
   * @param percentHard Percentage of clauses that should be hard
   * @return Randomly generated formula
   */
  private static Formula generateRandomFormula(int litPerClause, int totalLit, int totalClause,
                                               int percentHard)
  {
    Random generator = new Random();
    Formula f = new Formula();
    String[] litNames = new String[totalLit];
    for (int x = 0; x < totalLit; x++) {
      litNames[x] = "x" + x;
    }
    for (int i = 0; i < totalClause; i++) {
      String s = "";
      for (int j = 0; j < litPerClause; j++) {
        int litCode = generator.nextInt(totalLit * 2);
        if (litCode < totalLit) s += "!";
        s += litNames[litCode % totalLit] + " ";
      }
      f.addClause(new Clause(s, ((generator.nextInt(100) < percentHard) ? Double.POSITIVE_INFINITY
          : generator.nextDouble() * 100)));
    }

    return f;
  }

  public static void totalTest2()
  {
    BindingsAndBound b = new BindingsAndBound();
    Formula f = new Formula();
    f.addClause("!x1", 2);
    f.addClause("!x2", 3);
    f.addClause("!x3", 4);
    f.addClause("!x4", 5);
    f.addClause("!x5", 9);
    f.addClause("!x6", 3);
    f.addClause("!x7", 1);
    f.addClause("!x8", 3);
    f.addClause("!x9", 3);
    f.addClause("!x1 !x2", Double.POSITIVE_INFINITY);
    f.addClause("!x2 !x3", Double.POSITIVE_INFINITY);
    f.addClause("!x4 !x3", Double.POSITIVE_INFINITY);
    f.addClause("!x4 !x5", Double.POSITIVE_INFINITY);
    f.addClause("!x1 !x5", Double.POSITIVE_INFINITY);
    f.addClause("!x5 !x6", Double.POSITIVE_INFINITY);
    f.addClause("!x6 !x7", Double.POSITIVE_INFINITY);
    f.addClause("!x7 !x8", Double.POSITIVE_INFINITY);
    f.addClause("!x8 !x9", Double.POSITIVE_INFINITY);
    f.addClause("!x5 !x9", Double.POSITIVE_INFINITY);

    System.out.println(MinSatz.runMinSatz(f, b, null));
    System.out.println(MinSatz.optimalSat(f));
  }

  public static void optimalTest()
  {
    Formula f = new Formula();
    f.addClause("a a a a b c", 0);
    f.addClause("!a a !a b", 1);
    f.addClause("a !b", 2);
    f.addClause("a !c !c", 3);
    f.addClause("!a c", 4);
    f.addClause("b", 5);
    f.addClause("!c !b", Double.POSITIVE_INFINITY);
    f.addClause("b b", Double.POSITIVE_INFINITY);

    Map<String, Boolean> res = MinSatz.optimalSat(f);
    System.out.println("RESULT:");
    for (String s : res.keySet())
      System.out.println(s + ":" + res.get(s));
  }

  public static void totalTest()
  {
    BindingsAndBound b = new BindingsAndBound();
    Formula f = new Formula();
    f.addClause("a a a a b c", 0);
    f.addClause("!a a !a b", 1);
    f.addClause("a !b", 2);
    f.addClause("a !c !c", 3);
    f.addClause("!a c", 4);
    f.addClause("b", 5);
    f.addClause("!c !b", Double.POSITIVE_INFINITY);
    f.addClause("b b", Double.POSITIVE_INFINITY);

    System.out.println(MinSatz.runMinSatz(f, b, null));
  }

  public static void sanitizeTest()
  {
    BindingsAndBound b = new BindingsAndBound();
    Formula f = new Formula();
    f.addClause("a a a a b c", 0);
    f.addClause("!a a !a b", 1);
    f.addClause("a !b", 2);
    f.addClause("a !c !c", 3);
    f.addClause("!a c", 4);
    f.addClause("b", 5);
    f.addClause("!c !b", Double.POSITIVE_INFINITY);
    f.addClause("b b", Double.POSITIVE_INFINITY);
    f.propagate(null, b, false);

    System.out.println("end: " + f);
    System.out.println(b);
  }

  public static void upperBoundTest()
  {
    // example 2 in paper
    Formula f = new Formula();
    f.addClause("!x1", 2);
    f.addClause("!x2", 3);
    f.addClause("!x3", 4);
    f.addClause("!x4", 5);
    f.addClause("!x5", 6);
    f.addClause("!x1 !x2", Double.POSITIVE_INFINITY);
    f.addClause("!x2 !x3", Double.POSITIVE_INFINITY);
    f.addClause("!x3 !x4", Double.POSITIVE_INFINITY);
    f.addClause("!x4 !x5", Double.POSITIVE_INFINITY);
    f.addClause("!x1 !x5", Double.POSITIVE_INFINITY);
    System.out.println("formula " + f);
    System.out.println("UB2: " + f.overestimate());

    BindingsAndBound b = new BindingsAndBound();
    System.out.println(MinSatz.runMinSatz(f, b, null));
    Map<String, Boolean> res = MinSatz.optimalSat(f);
    System.out.println("RESULT:");
    for (String s : res.keySet())
      System.out.println(s + ":" + res.get(s));
  }

  public static void overestimateGraphBuildTest()
  {
    Formula f = new Formula();
    f.addClause("a b c", 0);
    f.addClause("!a b", 1);
    f.addClause("a !b", 2);
    f.addClause("a !c", 3);
    f.addClause("!a c", 4);
    f.addClause("b", 5);
    f.addClause("!c !b", Double.POSITIVE_INFINITY);
    f.addClause("a !b", Double.POSITIVE_INFINITY);
    f.overestimate();
  }

  public static void propagateTest()
  {
    Formula f = formulaTest();
    f.propagate(new Binding(new Literal("b", true), true), null, false);
    System.out.println("propagated:\n" + f);
  }

  public static Formula formulaTest()
  {
    Formula f = new Formula();
    f.addClause("a b c", 2);
    f.addClause("!a b", 4);
    f.addClause("!c !b", Double.POSITIVE_INFINITY);

    System.out.println(f);
    return f;
  }

  public static void graphTest()
  {
    Graph g = new Graph(5);

    g.addVertex(0, 2);
    g.addVertex(1, 3);
    g.addVertex(2, 4);
    g.addVertex(3, 5);
    g.addVertex(4, 6);

    g.addEdge(0, 1);
    g.addEdge(0, 4);
    g.addEdge(1, 2);
    g.addEdge(2, 3);
    g.addEdge(3, 4);

    System.out.println("UB: " + g.getUpperBound());
  }

  public static void graphTest2()
  {
    Graph g = new Graph(7);

    g.addVertex(0, 2);
    g.addVertex(1, 3);
    g.addVertex(2, 4);
    g.addVertex(3, 5);
    g.addVertex(4, 5);
    g.addVertex(5, 5);
    g.addVertex(6, 5);

    g.addEdge(0, 1);
    g.addEdge(0, 2);
    g.addEdge(0, 3);

    g.addEdge(1, 2);
    g.addEdge(1, 3);
    g.addEdge(1, 4);

    g.addEdge(2, 4);
    g.addEdge(2, 5);
    g.addEdge(2, 6);

    g.addEdge(3, 4);
    g.addEdge(3, 5);
    g.addEdge(3, 6);

    g.addEdge(4, 5);
    g.addEdge(4, 6);

    g.addEdge(5, 6);

    List<Vertex> sorted = g.sortedByDegree();

    System.out.println(sorted);
    System.out.println(g.maxClique(sorted));
  }
}
